Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    a__from(X)  → cons(mark(X),from(s(X)))
2:    a__head(cons(X,XS))  → mark(X)
3:    a__2nd(cons(X,XS))  → a__head(mark(XS))
4:    a__take(0,XS)  → nil
5:    a__take(s(N),cons(X,XS))  → cons(mark(X),take(N,XS))
6:    a__sel(0,cons(X,XS))  → mark(X)
7:    a__sel(s(N),cons(X,XS))  → a__sel(mark(N),mark(XS))
8:    mark(from(X))  → a__from(mark(X))
9:    mark(head(X))  → a__head(mark(X))
10:    mark(2nd(X))  → a__2nd(mark(X))
11:    mark(take(X1,X2))  → a__take(mark(X1),mark(X2))
12:    mark(sel(X1,X2))  → a__sel(mark(X1),mark(X2))
13:    mark(cons(X1,X2))  → cons(mark(X1),X2)
14:    mark(s(X))  → s(mark(X))
15:    mark(0)  → 0
16:    mark(nil)  → nil
17:    a__from(X)  → from(X)
18:    a__head(X)  → head(X)
19:    a__2nd(X)  → 2nd(X)
20:    a__take(X1,X2)  → take(X1,X2)
21:    a__sel(X1,X2)  → sel(X1,X2)
There are 23 dependency pairs:
22:    A__FROM(X)  → MARK(X)
23:    A__HEAD(cons(X,XS))  → MARK(X)
24:    A__2ND(cons(X,XS))  → A__HEAD(mark(XS))
25:    A__2ND(cons(X,XS))  → MARK(XS)
26:    A__TAKE(s(N),cons(X,XS))  → MARK(X)
27:    A__SEL(0,cons(X,XS))  → MARK(X)
28:    A__SEL(s(N),cons(X,XS))  → A__SEL(mark(N),mark(XS))
29:    A__SEL(s(N),cons(X,XS))  → MARK(N)
30:    A__SEL(s(N),cons(X,XS))  → MARK(XS)
31:    MARK(from(X))  → A__FROM(mark(X))
32:    MARK(from(X))  → MARK(X)
33:    MARK(head(X))  → A__HEAD(mark(X))
34:    MARK(head(X))  → MARK(X)
35:    MARK(2nd(X))  → A__2ND(mark(X))
36:    MARK(2nd(X))  → MARK(X)
37:    MARK(take(X1,X2))  → A__TAKE(mark(X1),mark(X2))
38:    MARK(take(X1,X2))  → MARK(X1)
39:    MARK(take(X1,X2))  → MARK(X2)
40:    MARK(sel(X1,X2))  → A__SEL(mark(X1),mark(X2))
41:    MARK(sel(X1,X2))  → MARK(X1)
42:    MARK(sel(X1,X2))  → MARK(X2)
43:    MARK(cons(X1,X2))  → MARK(X1)
44:    MARK(s(X))  → MARK(X)
Consider the SCC {22-44}. The constraints could not be solved.
Tyrolean Termination Tool  (17.44 seconds)   ---  May 3, 2006